Skip to content

[Merged by Bors] - feat(Module/Projective): direct sum of projective modules is projective#39764

Closed
vlad902 wants to merge 6 commits into
leanprover-community:masterfrom
vlad902:projective-directsum
Closed

[Merged by Bors] - feat(Module/Projective): direct sum of projective modules is projective#39764
vlad902 wants to merge 6 commits into
leanprover-community:masterfrom
vlad902:projective-directsum

Conversation

@vlad902

@vlad902 vlad902 commented May 24, 2026

Copy link
Copy Markdown
Collaborator

Open in Gitpod

@github-actions github-actions Bot added the t-algebra Algebra (groups, rings, fields, etc) label May 24, 2026
@github-actions

github-actions Bot commented May 24, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary ae42657234

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Projective.directSum
+ Projective.directSum_iff
+ component_comp_lof
+ component_comp_lof_same

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.
No changes to weak technical debt.

@vlad902 vlad902 mentioned this pull request May 24, 2026
Closed
themathqueen
themathqueen reviewed May 24, 2026
View reviewed changes
Comment thread Mathlib/Algebra/Module/Projective.lean Outdated
Comment thread Mathlib/Algebra/Module/Projective.lean Outdated
Comment thread Mathlib/Algebra/Module/Projective.lean Outdated
Comment thread Mathlib/Algebra/Module/Projective.lean Outdated
robin-carlier
robin-carlier reviewed May 24, 2026
View reviewed changes
Comment thread Mathlib/Algebra/Module/Projective.lean Outdated
Comment thread Mathlib/Algebra/Module/Projective.lean Outdated
@robin-carlier robin-carlier added the awaiting-author A reviewer has asked the author a question or requested changes. label May 24, 2026
robin-carlier
robin-carlier reviewed May 24, 2026
View reviewed changes
Comment thread Mathlib/Algebra/Module/Projective.lean Outdated
universe w v u

open LinearMap hiding id
open DirectSum hiding id id_apply

@robin-carlier robin-carlier May 24, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

note but not for this PR: this might mean there is a missing protected on DirectSum.id and DirectSum.id_apply.

@vlad902 vlad902 removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 24, 2026
robin-carlier
robin-carlier reviewed May 24, 2026
View reviewed changes

@robin-carlier robin-carlier left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

maintainer merge

@github-actions

github-actions Bot commented May 24, 2026

Copy link
Copy Markdown

🚀 Pull request has been placed on the maintainer queue by robin-carlier.

@mathlib-triage mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 24, 2026
@kbuzzard

kbuzzard commented May 25, 2026

Copy link
Copy Markdown
Member

Thanks!

bors merge

@mathlib-triage mathlib-triage Bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels May 25, 2026
mathlib-bors Bot pushed a commit that referenced this pull request May 25, 2026
@vlad902
feat(Module/Projective): direct sum of projective modules is projecti…
e96b5ef 
…ve (#39764)
@mathlib-bors

mathlib-bors Bot commented May 25, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title feat(Module/Projective): direct sum of projective modules is projective [Merged by Bors] - feat(Module/Projective): direct sum of projective modules is projective May 25, 2026
@mathlib-bors mathlib-bors Bot closed this May 25, 2026
b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026
@vlad902 @b-mehta
feat(Module/Projective): direct sum of projective modules is projecti…
bb1a852 
…ve (leanprover-community#39764)
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
@vlad902 @Bergschaf
feat(Module/Projective): direct sum of projective modules is projecti…
1734062 
…ve (leanprover-community#39764)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@themathqueen themathqueen themathqueen left review comments
@robin-carlier robin-carlier robin-carlier left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@vlad902 @kbuzzard @themathqueen @robin-carlier